Nuprl Lemma : append-cancellation-right 0,22

T:Type, asas'bscs:T List.
||as|| = ||as'||    (cs @ as) = (bs @ as' T List  cs = bs 
latex


Definitionsas @ bs, Prop, P  Q, {T}, P  Q, ||as||, x:AB(x), t  T, P & Q
Lemmaslength wf1, general-append-cancellation, append wf

origin